//import java.util.HashSet;
//
//import java.util.LinkedList;
//
//import java.util.List;
//
//import java.util.ListIterator;
//
//import java.util.Set;
//
//import org.apache.commons.collections.buffer.CircularFifoBuffer;
//
//import org.apache.commons.collections.comparators.FixedOrderComparator;
//
//import org.apache.commons.collections.list.CursorableLinkedList;
//
//import org.apache.commons.collections.map.LRUMap;
//
//import org.apache.commons.collections.map.MultiValueMap;
//
//import org.apache.commons.collections.set.ListOrderedSet;
//
//import junit.framework.TestCase;
//
//import sketch.ounit.Observer;
//
//import sketch.ounit.Values;
//
//import sketch.specs.annotation.TestSketch;
//
//import junit.framework.TestCase;
//
//public class TestExpansion extends TestCase {
//	@sketch.ounit.OUnit void rewriteSize(){
//	    sketch.instrumenter.Tracer.startMethod("rewriteSize");
//	    MultiValueMap map=new MultiValueMap();
//	    map.put("A","AA");
//	    sketch.instrumenter.Tracer.recordObservation(23,"map.size()");
//	    Observer.observeExpr(map.size());
//	    map.put("B","BB");
//	    sketch.instrumenter.Tracer.recordObservation(25,"map.size()");
//	    Observer.observeExpr(map.size());
//	    map.put("C","CC");
//	    sketch.instrumenter.Tracer.recordObservation(27,"map.size()");
//	    Observer.observeExpr(map.size());
//	    map.put("D","D");
//	    sketch.instrumenter.Tracer.recordObservation(29,"map.size()");
//	    Observer.observeExpr(map.size());
//	    sketch.instrumenter.Tracer.endMethod("rewriteSize");
//	  }
//	
//	void rewriteTestConstructorException0() {
//		try {
//			Integer i = Values.choose(0, -20);
//			{
//				{
//					new CircularFifoBuffer(i);
//					int k = 10;
//					k = 30;
//				}
//				int k = 40;
//			}
//		} catch (NullPointerException ex) {
//			int k = 60;
//			return;
//		}
//	}
//	
//	void testVariable() {
//		{
////			int i = 0;
//			for(int i = 0; i < 100; i++) {
//				System.out.println(i);
//			}
//			int i = 0;
//		}
//	}
//	
//	void testVariable2() {
//		{
//			for(int infor = 0; infor < 100; infor++) {
//				System.out.println(infor);
//			}
//			int infor = 0;
//		}
//	}
//
//	void rewriteTestConstructorException1() {
//		try {
//			Integer i = Values.choose(0, -20);
//			{
//				{
//					new CircularFifoBuffer(null);
//				}
//			}
//		} catch (NullPointerException ex) {
//			return;
//		}
//	}
//
//	void rewriteTestArrayListConstructor0() {
//		String[] keys = new String[] { "keys" };
//		List<String> list = new LinkedList<String>();
//		FixedOrderComparator foc;
//		{
//			{
//				foc = new FixedOrderComparator(keys);
//			}
//		}
//		foc.getUnknownObjectBehavior();
//	}
//
//	void rewriteTestArrayListConstructor1() {
//		String[] keys = new String[] { "keys" };
//		List<String> list = new LinkedList<String>();
//		FixedOrderComparator foc;
//		{
//			{
//				foc = new FixedOrderComparator(list);
//			}
//		}
//		foc.getUnknownObjectBehavior();
//	}
//
//	void rewriteTestDecorator0() {
//		try {
//			{
//				{
//					ListOrderedSet.decorate((Set) null);
//				}
//			}
//			fail();
//		} catch (IllegalArgumentException ex) {
//		}
//	}
//
//	void rewriteTestDecorator1() {
//		try {
//			{
//				{
//					ListOrderedSet.decorate((List) null);
//				}
//			}
//			fail();
//		} catch (IllegalArgumentException ex) {
//		}
//	}
//
//	void rewriteTestDecorator2() {
//		try {
//			{
//				{
//					ListOrderedSet.decorate(null, null);
//				}
//			}
//			fail();
//		} catch (IllegalArgumentException ex) {
//		}
//	}
//
//	void rewriteTestDecorator3() {
//		try {
//			{
//				{
//					ListOrderedSet.decorate(new HashSet(), null);
//				}
//			}
//			fail();
//		} catch (IllegalArgumentException ex) {
//		}
//	}
//
//	void rewriteTestDecorator4() {
//		try {
//			{
//				{
//					ListOrderedSet.decorate(null, new LinkedList());
//				}
//			}
//			fail();
//		} catch (IllegalArgumentException ex) {
//		}
//	}
//
//	void rewriteSize0() {
//		MultiValueMap map = new MultiValueMap();
//		String key = Values.choose("A", "B", "C", "D");
//		String value = Values.choose("AA", "BB", "CC", "D");
//		{
//			{
//				map.put(key, value);
//			}
//			{
//				{
//					Observer.observeExpr(map.totalSize());
//					Observer.observeExpr(map.size());
//				}
//			}
//			{
//				{
//					map.remove(key);
//				}
//			}
//		}
//	}
//
//	void rewriteSize1() {
//		MultiValueMap map = new MultiValueMap();
//		String key = Values.choose("A", "B", "C", "D");
//		String value = Values.choose("AA", "BB", "CC", "D");
//		{
//			{
//				map.put(key, value);
//			}
//			{
//				{
//					{
//						Observer.observeExpr(map.totalSize());
//					}
//				}
//			}
//			{
//				{
//					map.remove(key);
//				}
//			}
//		}
//	}
//
//	void rewriteSize2() {
//		MultiValueMap map = new MultiValueMap();
//		String key = Values.choose("A", "B", "C", "D");
//		String value = Values.choose("AA", "BB", "CC", "D");
//		{
//			{
//				map.put(key, value);
//			}
//			{
//				{
//					{
//						Observer.observeExpr(map.size());
//					}
//				}
//			}
//			{
//				{
//					map.remove(key);
//				}
//			}
//		}
//	}
//
//	void rewriteSize3() {
//		MultiValueMap map = new MultiValueMap();
//		String key = Values.choose("A", "B", "C", "D");
//		String value = Values.choose("AA", "BB", "CC", "D");
//		{
//			{
//				map.put(key, value);
//			}
//			{
//				{
//					Observer.observeExpr(map.totalSize());
//					Observer.observeExpr(map.size());
//				}
//			}
//			{
//				{
//					{
//						map.remove(key);
//					}
//				}
//			}
//		}
//	}
//
//	void rewriteSize4() {
//		MultiValueMap map = new MultiValueMap();
//		String key = Values.choose("A", "B", "C", "D");
//		String value = Values.choose("AA", "BB", "CC", "D");
//		{
//			{
//				map.put(key, value);
//			}
//			{
//				{
//					Observer.observeExpr(map.totalSize());
//					Observer.observeExpr(map.size());
//				}
//			}
//			{
//				{
//				}
//			}
//		}
//	}
//
//	void rewriteSize5() {
//		MultiValueMap map = new MultiValueMap();
//		String key = Values.choose("A", "B", "C", "D");
//		String value = Values.choose("AA", "BB", "CC", "D");
//		{
//			{
//				map.put(key, value);
//			}
//			{
//				{
//					{
//						Observer.observeExpr(map.totalSize());
//					}
//				}
//			}
//			{
//				{
//					{
//						map.remove(key);
//					}
//				}
//			}
//		}
//	}
//
//	void rewriteSize6() {
//		MultiValueMap map = new MultiValueMap();
//		String key = Values.choose("A", "B", "C", "D");
//		String value = Values.choose("AA", "BB", "CC", "D");
//		{
//			{
//				map.put(key, value);
//			}
//			{
//				{
//					{
//						Observer.observeExpr(map.totalSize());
//					}
//				}
//			}
//			{
//				{
//				}
//			}
//		}
//	}
//
//	void rewriteSize7() {
//		MultiValueMap map = new MultiValueMap();
//		String key = Values.choose("A", "B", "C", "D");
//		String value = Values.choose("AA", "BB", "CC", "D");
//		{
//			{
//				map.put(key, value);
//			}
//			{
//				{
//					{
//						Observer.observeExpr(map.size());
//					}
//				}
//			}
//			{
//				{
//					{
//						map.remove(key);
//					}
//				}
//			}
//		}
//	}
//
//	void rewriteSize8() {
//		MultiValueMap map = new MultiValueMap();
//		String key = Values.choose("A", "B", "C", "D");
//		String value = Values.choose("AA", "BB", "CC", "D");
//		{
//			{
//				map.put(key, value);
//			}
//			{
//				{
//					{
//						Observer.observeExpr(map.size());
//					}
//				}
//			}
//			{
//				{
//				}
//			}
//		}
//	}
//
//	void rewriteCursorNextIndexAddNext0() {
//		CursorableLinkedList list = new CursorableLinkedList();
//		Integer[] array = Values.exhaust(1, 2, 3, 4);
//		for (int i : array) {
//			list.add(i);
//		}
//		CursorableLinkedList.Cursor it = list.cursor();
//		Observer.observeExpr(it.next());
//		Observer.observeExpr(it.nextIndex());
//		Integer add = Values.choose(1, 2, 3, 4);
//		{
//			{
//				list.add(add);
//			}
//		}
//		{
//			Observer.observeExpr(it.next());
//			Observer.observeExpr(it.nextIndex());
//		}
//	}
//
//	void rewriteCursorNextIndexAddNext1() {
//		CursorableLinkedList list = new CursorableLinkedList();
//		Integer[] array = Values.exhaust(1, 2, 3, 4);
//		for (int i : array) {
//			list.add(i);
//		}
//		CursorableLinkedList.Cursor it = list.cursor();
//		Observer.observeExpr(it.next());
//		Observer.observeExpr(it.nextIndex());
//		Integer add = Values.choose(1, 2, 3, 4);
//		{
//			{
//				list.remove(add);
//			}
//		}
//		{
//			Observer.observeExpr(it.next());
//			Observer.observeExpr(it.nextIndex());
//		}
//	}
//
//	void rewriteCursorNextIndexAddNext2() {
//		CursorableLinkedList list = new CursorableLinkedList();
//		Integer[] array = Values.exhaust(1, 2, 3, 4);
//		for (int i : array) {
//			list.add(i);
//		}
//		CursorableLinkedList.Cursor it = list.cursor();
//		Observer.observeExpr(it.next());
//		Observer.observeExpr(it.nextIndex());
//		Integer add = Values.choose(1, 2, 3, 4);
//		{
//			list.add(add);
//			list.remove(add);
//		}
//		{
//			{
//				Observer.observeExpr(it.next());
//			}
//			{
//				Observer.observeExpr(it.nextIndex());
//			}
//		}
//	}
//
//	void rewriteCursorNextIndexAddNext3() {
//		CursorableLinkedList list = new CursorableLinkedList();
//		Integer[] array = Values.exhaust(1, 2, 3, 4);
//		for (int i : array) {
//			list.add(i);
//		}
//		CursorableLinkedList.Cursor it = list.cursor();
//		Observer.observeExpr(it.next());
//		Observer.observeExpr(it.nextIndex());
//		Integer add = Values.choose(1, 2, 3, 4);
//		{
//			{
//				list.add(add);
//			}
//		}
//		{
//			{
//				Observer.observeExpr(it.next());
//			}
//			{
//				Observer.observeExpr(it.nextIndex());
//			}
//		}
//	}
//
//	void rewriteCursorNextIndexAddNext4() {
//		CursorableLinkedList list = new CursorableLinkedList();
//		Integer[] array = Values.exhaust(1, 2, 3, 4);
//		for (int i : array) {
//			list.add(i);
//		}
//		CursorableLinkedList.Cursor it = list.cursor();
//		Observer.observeExpr(it.next());
//		Observer.observeExpr(it.nextIndex());
//		Integer add = Values.choose(1, 2, 3, 4);
//		{
//			{
//				list.remove(add);
//			}
//		}
//		{
//			{
//				Observer.observeExpr(it.next());
//			}
//			{
//				Observer.observeExpr(it.nextIndex());
//			}
//		}
//	}
//
//	void rewriteListListIteratorNextRemovePrevious0() {
//		List list = new LinkedList();
//		ListIterator it = list.listIterator();
//		list.add(1);
//		list.add(2);
//		list.add(3);
//		int index = Values.choose(0, 1, 2);
//		{
//			{
//				it.remove();
//			}
//			{
//				index++;
//			}
//		}
//		Object o = list.get(index);
//		Object o1 = null;
//		while (index-- > 0) {
//			o1 = it.next();
//		}
//		Observer.observeExpr(o, o1);
//	}
//
//	void rewriteListListIteratorNextRemovePrevious1() {
//		List list = new LinkedList();
//		ListIterator it = list.listIterator();
//		list.add(1);
//		list.add(2);
//		list.add(3);
//		int index = Values.choose(0, 1, 2);
//		{
//		}
//		Object o = list.get(index);
//		Object o1 = null;
//		while (index-- > 0) {
//			o1 = it.next();
//		}
//		Observer.observeExpr(o, o1);
//	}
//
//	void rewriteLRUMap0() {
//		LRUMap map = new LRUMap(3);
//		map.put(1, 2);
//		map.put(2, 3);
//		map.put(3, 4);
//		int key = Values.choose(1, 2, 3, 4);
//		int value = Values.choose(5, 6, 7, 8);
//		if (key > value) {
//			int notreachable = Values.choose(5, 6, 7, 9);
//		}
//		{
//			{
//				{
//					map.put(1, 5);
//					Observer.observeExpr(map.size());
//					Observer.observeExpr(map.isEmpty(), false);
//					Observer.observeExpr(map.containsKey(1), true);
//					Observer.observeExpr(map.containsKey(5), false);
//				}
//			}
//			{
//				{
//					map.put(2, 6);
//					Observer.observeExpr(map.size());
//					Observer.observeExpr(map.isEmpty(), false);
//					Observer.observeExpr(map.containsKey(2), true);
//					Observer.observeExpr(map.containsKey(6), false);
//				}
//			}
//			{
//				{
//					map.put(3, 7);
//					Observer.observeExpr(map.size());
//					Observer.observeExpr(map.isEmpty(), false);
//					Observer.observeExpr(map.containsKey(3), true);
//					Observer.observeExpr(map.containsKey(7), false);
//				}
//			}
//			{
//				{
//					map.put(4, 8);
//					Observer.observeExpr(map.size());
//					Observer.observeExpr(map.isEmpty(), false);
//					Observer.observeExpr(map.containsKey(4), true);
//					Observer.observeExpr(map.containsKey(8), false);
//				}
//			}
//		}
//		if (key > value) {
//			int notreachable2 = Values.choose(5, 6, 7, 9);
//		}
//	}
//}
